#!/bin/bash
#===============================================================================
# config-local.sh
#
# Configuration settings that pertain to the local environment
#===============================================================================

HOME_DIR=/Users/jaco/Public/Dropbox
REDIS_LOCAL_DIR=${HOME_DIR}/RESEARCH/REDIS/redis-2.8.19/src
WORKSPACE_DIR=${HOME_DIR}/WORKSPACE
JPF_DISTRIB_LOCAL_DIR=${WORKSPACE_DIR}/jpf-distrib
JPF_SYMBC_LOCAL_DIR=${WORKSPACE_DIR}/jpf-symbc
JPF_CORE_LOCAL_DIR=${WORKSPACE_DIR}/jpf-core
GREEN_LOCAL_DIR=${WORKSPACE_DIR}/green

#-------------------------------------------------------------------------------
# In case someone tries to execute this script
#-------------------------------------------------------------------------------

echo "!!! You are not supposed to run this shell script!"

#===============================================================================
# End of config-local.sh
#===============================================================================
